『Homotopy Type Theory 入門』
1. どんなもの？
type-chekingを決定可能にしたい？
2. 先行研究と比べてどこがすごい？
3. 技術や手法のキモはどこ？
4. どうやって有効だと検証した？
5. 議論はある？
6. 次に読むべき論文は？
7. 参考文献
1. イントロダクション
帰納的型の拡張で、単位円周や球面などの空間を表す型や、自由群や商型などの要素間の同一視が必要な型を構成できる 1.1 型と空間
Univalent Foundations program
HoTT の基本的なアイディアは、型を空間、要素を点と解釈すること
等式型 a =A a′ を点 a から点 a′ への道の空間
uniqueness of identity proofs (UIP)
数学的対象$ a が型$ a を持つことを$ a : A
$ a は型$ A の要素であるとも言う
$ a は変数$ x に依存するかもしれないときは$ a[x] と書く
代入(substitution)という操作でもある
二つの数学的対象が等しい場合は$ a \equiv b
型$ A, B 、$ A から$ B への関数型(function type)を$ A \to B
$ x : A
変数$ x : A 、要素$ b[x] : B があったときに、λ-抽象は $ λ(x : A).b[x] : A \to B
要素$ f : A \to B と$ a : A があったときに、関数適用(application)$ f(a) : A \to B が定義される
α同値
β同値
η同値
関連